#include "buffer_underflow.hpp"

buffer_underflow::buffer_underflow(const CFGvisitorFlatInfo& _flat, DetectionSign& _ds) 
:	flat(_flat), ds(_ds)
{
}
	
set<label_t> buffer_underflow::underflow() {
	set<label_t> U;	// set of labels in which underflow can occur

	for_each(this->flat.labels, [&U, this](CFGvertex* n){
		label_t ell = n->label();
		
		ASTvisitorGetArrays ga;
		set<array_element*> arrays = ga.convert(this->getPayload(n));

		for (auto it = arrays.begin(); it != arrays.end(); ++it) {
			array_element* ae = *it;
			
			DS tmp = this->ds.MFP_entry(ell);
			ASTvisitorAs As(tmp);
			Interval ia = As.get_interval(ae->index);

			const bool can_be_neg = (ia.lower() < 0 || ia.upper() < 0);
			if (can_be_neg) {U.insert(ell);}
		}
	});

	return U;
}

ASTnode* buffer_underflow::getPayload(label_t ell0) const {
	return this->getPayload(flat.labels[ell0]);
}

ASTnode* buffer_underflow::getPayload(CFGvertex *n) const {
	ASTnode *a = NULL;
	if (TRY_TYPE(box*, b, n)) {
		a = b->payload;
	}
	if (TRY_TYPE(diamond*, d, n)) {
		a = d->condition;
	}
	assert(a);
	return a;
}
